\begin{tabbing}
sends1{-}p(${\it es}$;$x$;$A$;$k$;$B$;$l$;${\it tg}$;$T$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=((es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq$r $A$)\+
\\[0ex]\& (\=$\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex](es{-}loc(${\it es}$; $e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $B$))
\-\\[0ex]\& ($\forall$$e$:es{-}E(${\it es}$). (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=($\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex](es{-}loc(${\it es}$; $e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\exists$\=$L$:\{${\it e'}$:es{-}E(${\it es}$)$\mid$ es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd\}  List\+
\\[0ex]((\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex](${\it e'}$ $\in$ $L$ $\in$ es{-}E(${\it es}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)\+
\\[0ex]c$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$))))
\-\-\\[0ex]\& (\=$\forall$$e_{1}$:es{-}E(${\it es}$), $e_{2}$:es{-}E(${\it es}$).\+
\\[0ex]$e_{1}$ before $e_{2}$ $\in$ $L$ $\in$ es{-}E(${\it es}$) $\Rightarrow$ es{-}locl(${\it es}$; $e_{1}$; $e_{2}$))
\-\\[0ex]\& \=map($\lambda$${\it e'}$.es{-}val(${\it es}$; ${\it e'}$);$L$)\+
\\[0ex]=
\\[0ex]$f$(es{-}when(${\it es}$; $x$; $e$),es{-}val(${\it es}$; $e$))
\\[0ex]$\in$ ($T$ List))))
\-\-\-\-
\end{tabbing}